es:ES, L1, L2:(E List), i:Id.
loc-on-path(es;i;L1 @ L2)  (loc-on-path(es;i;L1)  loc-on-path(es;i;L2)) 

latex

Definitions	s = t, t  T, x:AB(x), x:A. B(x), loc-on-path(es;i;L), left + right, , P  Q, ES, type List, Id, P  Q, P  Q, x:A  B(x), P & Q, P  Q, (x  l), loc(e), x.A(x), map(f;as), as @ bs, s ~ t, E
Lemmas	event system wf, es-E wf, map append sq, iff functionality wrt iff, member append, iff wf, rev implies wf, Id wf, l member wf, loc-on-path wf